Nuprl Lemma : d-partial-world_wf
0,22
postcript
pdf
D
:Dsys,
s
:(
i
:Id
M(
i
).state),
t
:
,
f
:(
t
(
i
:Id
d-world-state(
D
;
i
))).
d-partial-world(
D
;
f
;
t
;
s
)
World
latex
Definitions
t
T
,
1of(
t
)
,
x
:
A
.
B
(
x
)
,
Msg(
M
)
Lemmas
lsrc
wf
,
d-m
wf
,
ma-dout
wf
,
subtype
rel
self
,
nat
wf
,
Msg
wf
,
mlnk
wf
,
w-automaton
wf
,
ma-ds
wf
,
ma-da
wf
,
locl
wf
,
top
wf
,
action
wf
,
w-action-dec
wf
origin
D:Dsys, s:(i:Id
M(i).state), t:
, f:(t(i:Idd-world-state(D;i))).
World D:Dsys, s:(i:IdM(i).state), t:, f:(t(i:Idd-world-state(D;i))).
World Tx:A. B(x)